$\forall$$e$:EventsWithValues, $p$:AtomFreeDecls($e$). EVal\_to\_ES\{i:l\}($e$,$p$) $\in$ ES0